Concerning the problem that microservice composition platform is short of analysis and verification of Quality of Service (QoS) indicators, a formal verification method based on model checking was proposed to analyze and evaluate the factors that affect the microservice composite platform performance. First, the service resource configuration process of microservice composition was divided into three phases:service request, configuration and service execution. These three phases were implemented by three modules:service request queue, resource configurator of service requests and virtual machine for providing service resources. After that, the implementation processes of the three modules were modeled as Labelled Markov Reward Models (LMRM), and the global model of microservice composition process was obtained by using a synchronization concept similar to the process algebra. Then, the logic formula of continuous random reward logic was used to describe the expected QoS indicators. Last, the formal model and logic formula were regarded as the input of model detection tool PRISM to obtain the verification results. Experimental results prove that LMRM can realize the QoS verification and analysis as well as the construction of microservice composite platform.